@echo off
SetLocal EnableDelayedExpansion

set ROOT_DIR=%~dp0
set JAVA_EXE=java 

REM Attention: 'where' might not be available on all Windows versions
call where %JAVA_EXE% > NUL
if not %ERRORLEVEL%==0 (
	echo Java could not be started.
	goto :exit_with_error
)

if "%IVY_HOME%"=="" (
	REM Environment variable IVY_HOME not pre-defined; checks on classpath below will catch a false definition here
	set IVY_HOME=%USERPROFILE%\.ivy2
)

if "%SBT_HOME%"=="" (
	REM Environment variable SBT_HOME not pre-defined; checks on classpath below will catch a false definition here
	set SBT_HOME=%USERPROFILE%\.sbt
)

set BOOGIE_EXE=C:\boogie\Binaries\Boogie.exe
if not "%BOOGIE_HOME%"=="" set BOOGIE_EXE="%BOOGIE_HOME%\Boogie.exe"

set CHALICE_SCALA_VERSION=2.10.0
set CHALICE_SCALA_VERSION_TARGET_DIR=2.10

REM Set classpath elements
REM set __CP.SCALA_LIB="%IVY_HOME%\cache\org.scala-lang\scala-library\jars\scala-library-%CHALICE_SCALA_VERSION%.jar"
set __CP.SCALA_LIB="%SBT_HOME%\boot\scala-%CHALICE_SCALA_VERSION%\lib\scala-library.jar"
set __CP.CHALICE="%ROOT_DIR%target\scala-%CHALICE_SCALA_VERSION_TARGET_DIR%\classes"

REM Assemble classpath and check if all classpath elements exist
set CP=
for /f "tokens=2* delims=.=" %%A in ('set __CP.') do (
	if not exist %%B (
		echo %%B does not exist.
		goto :exit_with_error
	) else (
		set CP=!CP!;%%B
	)
)

REM Chalice main class
set CHALICE_MAIN=chalice.Chalice

REM Chalice command line options
set CHALICE_OPTS=
set CHALICE_OPTS=%CHALICE_OPTS% /boogieOpt:nologo
set CHALICE_OPTS=%CHALICE_OPTS% /boogieOpt:noinfer
set CHALICE_OPTS=%CHALICE_OPTS% /boogie:%BOOGIE_EXE%
set CHALICE_OPTS=%CHALICE_OPTS% %*

REM Assemble main command
set CMD=%JAVA_EXE% -cp %CP% -Xss16M %CHALICE_MAIN% %CHALICE_OPTS%

REM echo.
REM echo %CMD%
REM echo.

call %CMD%

exit /B 0


:exit_with_error
exit /B 1
